Nuprl Lemma : rationals_wf
11,40
postcript
pdf
rationals
Type
latex
Definitions
x
,
y
.
t
(
x
;
y
)
,
prop{i:l}
,
rationals
,
t
T
,
x
(
s1
,
s2
)
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
qeq-equiv
,
btrue
wf
,
qeq
wf
,
bool
wf
,
int
nzero
wf
,
b-union
wf
,
quotient
wf
origin
Type Type 
x,y. t(x;y) T
Q
x:A. B(x)